#include <stdlib.h>
#include <stdio.h>


/*@ pattern doublelinkedlist<(val,va,v),next,prev> dllist */
struct dllistNode {
	int val;
	struct dllistNode* next;
	int va;
	struct dllistNode* prev;
	int v;
};

/*@ pattern singlelinkedlist<next> list */
/*@ pattern singlelinkedlist<(val),next> listrd */
struct listNode {
	int val;
	struct listNode * next;
};

/*@ pattern singlelinkedlist<(val),nexts> lists */
struct listNodes {
	int val;
	struct listNodes * nexts;
};

/*@ pattern singlelinkedlist<(v,va,val),nextd> listd */
struct listNoded {
	int v;
	int va;
	int val;
	struct listNoded * nextd;
};


struct listNode* reverse(struct listNode *x)
//@ pre  <heap> list(x)(A), H </heap>
//@ post <heap> list(p)(rev(A)), H </heap> /\ returns(p)
{
	struct listNode *p;
	struct listNode *y;
	
	p = 0 ;
	/*@ invariant <heap> list(p)(?B), list(x)(?C), H </heap>
	 /\ A = rev(?B) @ ?C */
	while(x) {
		y = x->next;
		x->next = p;
		p = x;
		x = y;
	}
	
	return p;
}

struct listNode* create(int n)
{
	struct listNode *x;
	struct listNode *y;
	x = 0;
	while (n)
	{
		y = x;
		x = (struct listNode*)malloc(sizeof(struct listNode));
		x->val = n;
		x->next = y;
		n -= 1;
	}
	return x;
}

void destroy(struct listNode* x)
//@ pre  <heap> list(x)(?A), H </heap>
//@ post <heap> H </heap>
{
	struct listNode *y;
	
	//@ invariant <heap> list(x)(?A), H </heap>
	while(x)
	{
		y = x->next;
		free(x);
		x = y;
	}
}


void print(struct listNode* x)
//@ pre  <heap>  list(x)(A), H </heap><out> B </out> /\ x = x0
//@ post <heap> list(x0)(A), H </heap><out> B @ A </out>
{
	/*@ invariant <heap> lseg(x0,x)(?A1), list(x)(?A2), H </heap>
	 <out> B @ ?A1 </out> /\ A = ?A1 @ ?A2 */
	while(x)
	{
		printf("%d ",x->val);
		x = x->next;
	}
	printf("\n"); 
}


int main()
{
	struct listNode *x;
	struct listNode *y;
	
	x = create(5);
	//@ assert <heap> list(x)([1, 2, 3, 4, 5]) </heap>
	x = reverse(x);
	//@ assert <heap> list(x)([5, 4, 3, 2, 1]) </heap>
	destroy(x);
	return 0;
}


//@ var n : Int
//@ var A, B, C : Seq
//@ var H : MapItem

